e leaks x to e'
== a:Atom1
== (loc(e) || a
== & (state when e\\x:state@loc(e)\\x||a)
== & e receives || a
== & ((isrcv(e')) c (sender(e') = e & (val(e'):valtype(e')||a)))) 

latex

---

clarification:

es-leaks(es;e;x;e')
== a:Atom1
== (es-atom(es;es-loc(es; e);a)
== & (free-from-atom{1}(es-state-without(es;es-loc(es; e);x);es-state-when-without(es;e;x);a))
== & es-rcv-atom(es;e;a)
== & ((es-isrcv(es; e'))
== & (c (es-sender(es; e') = e  es-E(es)
== & (c & (free-from-atom{1}(es-valtype(es; e');es-val(es; e');a))))) 

latex

Definitions	x:A. B(x), Atom$n, state@i\\x, loc(e), state when e\\x, e receives || a, A c B, b, isrcv(e), P & Q, s = t, E, sender(e), A, x:T||a, valtype(e), val(e)
FDL editor aliases	es-leaks